Brief introduction of Gödel's Incompleteness Theorems
はじめに
論理
ある言語$ \mathcal{L}
$ \mathscr{S}の要件
ここでは，$ \mathscr{S}は少なくとも次の要件を満たす．
定数記号$ \mathbf{0}が存在する．
変数$ x,y,z,w,\phi,\psiなど
表記上の問題であり全てを$ v_1,v_2,\dotsと置いても良い
$ x,y,z,wなどは数項などのために使う
$ \phi,\psiなとは自由変数のために使う
後者演算子$ S(x)が存在する．
論理関数$ \to,\lnotが存在する
$ A \lor B := \lnot A \to B
$ A \land B := \lnot (\lnot A \lor \lnot B)
述語$ =が存在する．
量化子$ \exists
Gödel数
$ \mathscr{S}の表現$ Eに一意な自然数$ g(E)を割り振ることが出来る
$ g(E)は$ \Nと1対1対応であることが望ましい
逆に，自然数$ xに対して対応する表現を$ E_xで表す．
自然数$ xに対して$ \mathscr{S}の数項$ \bar{x} = \underbrace{S(S(\cdots S}_{x \text{ times}}(\mathbf{0}) \cdots )と定める．
例えば，
$ \overline{0} = \mathbf{0}
$ \overline{2} = s(s(\mathbf{0}))
自然数上の関数$ f(x_1,\dots,x_n)=yが$ \mathscr{S}で表現可能であるとは，
$ n+1個の自由変数を取る$ \mathscr{S}の論理式$ A_f\lbrack \overline{x_1},\dots,\overline{x_n},\overline{y} \rbrackが次の条件を満たす．
0. 変数$ \overline{x_1},\dots,\overline{x_n},\overline{y}は数項である．
1.$ f(x_1,\dots,x_n)=yのとき，論理式$ A_f\lbrack \overline{x_1},\dots,\overline{x_n},\overline{y} \rbrackは$ \mathscr{S}で証明可能である．
解が存在することを表している
2. $ \forall\overline{x_1},\dots,\forall\overline{x_n},\forall\overline{y},\forall\overline{z} .\left( A_f\lbrack \overline{x_1},\dots,\overline{x_n},\overline{y}\rbrack \land A_f\lbrack\overline{x_1},\dots,\overline{x_n},\overline{z} \rbrack \to \overline{y} = \overline{z} \right) が$ \mathscr{S}で証明可能
解の唯一性を表している
そのような$ \mathscr{S}の論理式$ A_fが存在するとき，$ A_fは$ f(x_1,\dots,x_n)=yを$ \mathscr{S}で表現しているという．
以下，誤解がなければ$ \mathscr{S}は省略する．
表現補題
自然数上の関数$ f(x_1,\dots,x_n)が原始再帰的関数である． $ \iff$ f(x_1,\dots,x_n) = yを表現する$ \mathscr{S}の論理式$ A_f\lbrack \overline{x_1},\dots,\overline{x_n},\overline{y} \rbrackが存在する．
証明の関数
以下の自然数上の関数は$ 0または$ 1を返すとする．
$ 0ならそうであり，$ 1ならそうではない．
$ x,y_1,\dots,y_nは自然数とする．
$ \mathrm{isAxiom}(x)
表現$ E_xは，$ \mathscr{S}のいずれかの公理である．
$ \mathrm{isIntro}(x,y_1,\dots,y_n)
表現$ E_xは，$ \mathscr{S}のいずれかの推論規則によって式$ E_{y_1},\dots,E_{y_n}から推論される論理式である．
$ \mathrm{isProof}(x)
表現$ E_xは，$ \mathscr{S}の証明である．
$ \mathrm{isProofOf}(x,y)
表現$ E_yは，表現$ E_xの$ \mathscr{S}での証明を表している．
証明可能性
仮定1. $ \mathrm{isProofOf}(x,y)が原始再帰的関数であるとする． 表現補題より，$ z = \mathrm{isProofOf}(x,y)を表現する自由変数が3つの論理式$ A_\mathrm{isProofOf}\lbrack \overline{x},\overline{y},\overline{z}\rbrackが存在する．
長いので，以下では論理式$ \mathrm{isProofOf}\lbrack \overline{x},\overline{y},\overline{z}\rbrackと表す．
自然数$ xに対して，自由変数が1つの論理式$ \mathrm{Provable}\lbrack \bar{x} \rbrackを
$ \mathrm{Provable}\lbrack \bar{x} \rbrack := \exists \overline{y}.\mathrm{isProofOf}\lbrack \overline{x},\overline{y},\overline{0}\rbrackと置く．
「$ 0 = \mathrm{isProofOf}(x,y)となる自然数$ yが存在する」
すなわち，「表現$ E_xの$ \mathscr{S}の証明が存在する」あるいは「表現$ E_xは$ \mathscr{S}で証明可能である」を表している．
対角化関数
自然数$ xは，自由変数$ \phiを一つ持つ何らかの論理式$ E_x \left\lbrack \phi \right\rbrackのGödel数であるとする． $ \phiに$ \overline{x}を代入した$ E_x\left\lbrack\overline{x}\right\rbrack，すなわち$ E_x\left\lbrack\overline{g\left(E_x\lbrack\phi\rbrack\right)}\right\rbrackのGödel数を$ \mathrm{diag}(x)とする．
すなわち，$ \mathrm{diag}(x) = g\left( E_x\left\lbrack\overline{g\left(E_x\lbrack\phi\rbrack\right)}\right\rbrack \right)である．
仮定2. $ \mathrm{diag}(x)は原始再帰的関数であると仮定する． 表現補題より，$ y = \mathrm{diag}(x)を表現する自由変数が2つの論理式$ A_\mathrm{diag}\lbrack \overline{x},\overline{y}\rbrackが存在する．
長いので，以下では論理式$ \mathrm{Diag}\lbrack \overline{x},\overline{y}\rbrackと表す．
Gödel文$ Gの構成
自由変数$ \overline{x}をただ一つ持つ$ \mathscr{S}の論理式$ A\lbrack \overline{x} \rbrackを以下のように定義する．
$ A\lbrack \overline{x} \rbrack := \exists \overline{y}\left(\mathrm{Diag}\left\lbrack \overline{x},\overline{y} \right\rbrack \land \lnot\mathrm{Provable}\lbrack \overline{y} \rbrack \right)
$ \mathrm{Diag}\lbrack \overline{x},\overline{y} \rbrack
自由変数を一つ含む論理式$ E_xがあり，$ x = g\left( E_x \right)である．
$ E_xに自分自身のGödel数の数項$ \overline{ g\left( E_x \right)}を代入して出来る文$ E_x\left\lbrack \overline{ g\left( E_x \right)} \right\rbrack
文$ E_x\left\lbrack \overline{ g\left( E_x \right)} \right\rbrackのGödel数が$ yである．
すなわち，自然数$ y = g \left( E_x\left\lbrack \overline{ g\left( E_x \right)} \right\rbrack \right)でる．
よって$ E_yは文$ E_x\left\lbrack \overline{ g\left( E_x \right)} \right\rbrackである
$ \lnot\mathrm{Provable}\lbrack \overline{y} \rbrack
すなわち，文$ E_yの$ \mathscr{S}での証明は存在しない．
文$ Gを，論理式$ A\left\lbrack \overline{x} \right\rbrackの自由変数として自分自身$ A\left\lbrack \overline{x} \right\rbrackのGödel数を代入した文とする．
すなわち，$ G := A\left\lbrack \overline{g \left( A\lbrack \overline{x} \rbrack \right)} \right\rbrackである．
$ g(G) = g\left(A\left\lbrack \overline{g \left( A\lbrack \overline{x} \rbrack \right)} \right\rbrack \right) = \mathrm{diag}(g(A\lbrack\overline{x}\rbrack))．
$ Gを展開する．
$ G \Leftrightarrow \exists \overline{y}\left(\mathrm{Diag}\left\lbrack \overline{g \left( A\lbrack \overline{x} \rbrack \right)},\overline{y} \right\rbrack \land \lnot\mathrm{Provable}\lbrack \overline{y} \rbrack \right)
$ \mathrm{Diag}\left\lbrack \overline{g \left( A\lbrack \overline{x} \rbrack \right)},\overline{y} \right\rbrack
$ y = \mathrm{diag}\left(g \left( A\lbrack \overline{x} \rbrack \right) \right)を表現している
ところで，$ \mathrm{diag}\left(g \left( A\lbrack \overline{x} \rbrack \right) \right)は$ g(G)であることを確認した．
すなわち，$ y = g(G)である．
よって，$ E_yは文$ Gである．
$ \lnot\mathrm{Provable}\left\lbrack \overline{y} \right\rbrack
$ \Leftrightarrow \lnot\mathrm{Provable}\left\lbrack \overline{g\left(G\right)} \right\rbrack
すなわち，$ Gの$ \mathscr{S}での証明は存在しない．
すなわち，文$ Gは，
「$ \mathscr{S}で証明不可能な文$ Gが存在する」ということを$ \mathscr{S}上で主張（自己言及）している． $ \mathscr{S} := \mathscr{P.A.}として実装
$ \mathscr{S}をPeano算術$ \mathscr{P.A.}として，$ \text{isAxiom},\text{isIntro}などを実装する．